'''
Created on 2011-04-25

@author: kacper
'''
from logger.logger import instLog, instLogFun
from dataStructs.definitions import NotFormula, Relation, Var
from copy import deepcopy
log = instLog("Resloution")
logFun = instLogFun(log)

def f(*args): pass
#log=f

from dataStructs.unify import  BrutefindUnify

def removeReptitions(clouse):
    return [x for x in set(clouse)]




states_dict =set()

def linearResolution(goal, kb,Maxdepth= 10, trace=None):
    states_dict.clear()
    for x in xrange(3,Maxdepth):
        while trace: trace.pop()
        for res in _linRes(goal, kb, x, trace):
            log("funny res", res)
            yield res
            while trace: trace.pop()



#states = { "succes":1, "failure":-1 , "undef":0, "maxdepth":-2 }
succes = 1
failure =-1
undef=0
maxdepth = -2
state = undef


def removeDefRepetions(L):
    if L:
        L.sort()
        last = L[-1]
        for i in range(len(L)-2, -1, -1):
            if last == L[i]:
                del L[i]
            else:
                last = L[i]
    return L

def _linRes(goals, knowledgeBase, depth, trace=None, right =0):
    tabulation = "".join( map( lambda x: " ", range(10-depth)) )

    if goals == []:
        yield [[]]
        return
     
    if  depth == 0:
        state = maxdepth
        return
    
    # goal =[  [[~p(b,l), ~x], [[]] ], [[~p(b,l), ~y], [[]]] ]
    # goal = [ g0, g1, g2 ... ]
    # g_i = [ or_clouse , def_clouse   ]
    # or_clouse = [t1,t2,t3, ... ] 


    log(tabulation,"in _linRes ")
    log(tabulation,"depth", depth)

    
    goalClouse = goals[0]
    # goalDef = [[[]]]
    goal, goalDef = goalClouse[0], goalClouse[1]
    log(tabulation,"goal, goalDef ", goal, goalDef) 
    tail = goals[1:]
    log(tabulation,"tail", tail)
    
    if goal == []:
        log(tabulation,"PROO Found")
        if trace != None:
            trace += [ "END OF PROOF"]
        yield goalDef
        return
    
    if (str(goal), right) in states_dict:
        return
    states_dict.add((str(goal), right))
    
    #fetch rest of results
    #result = [ OrCluse , OrClouse, ..,]
 
    for result in _linRes(tail, knowledgeBase, depth, trace, right+1):
        
        #log("knowledgebase",knowledgeBase )
        # knowledgebase = [ [ or_clouse, def_clouse] , ...  ]
        for factClouse in knowledgeBase:
            fact, factDef = factClouse[0], factClouse[1]
            
        #   log("all  fact, factDef", fact, factDef)
     
            for mgu in BrutefindUnify(fact, goal):
                posInFact, posInGoal = mgu


                log(tabulation,"fact, factDef ", fact, factDef)
                
                #cut parts of fact and goal and marge                
                newGoal = (goal[:posInGoal] + goal[posInGoal+1:] 
                            + fact[:posInFact] + fact[posInFact+1:])
                
                newGoal  = deepcopy(newGoal)
 
                
                newGoal = removeReptitions(newGoal) 
                
                
                if trace != None:
                    trace += [( "g",goal[posInGoal], "f",fact[posInFact],"ng", newGoal)]

                
                log(tabulation,"newGoal", newGoal)
                #pack newGola
                newGoalDef = goalDef+factDef
                
                
                newGoalDef = removeDefRepetions(newGoalDef)
                
                newGoalClouse = [ newGoal, newGoalDef]
                
                newGoals = [newGoalClouse]
                
                log(tabulation,"newGoals", newGoals)
                
                for inDepthRes in _linRes(newGoals, knowledgeBase, depth-1, trace, right +1):
                    log("inDepthRes",removeDefRepetions(inDepthRes + result))
                    yield removeDefRepetions(inDepthRes + result)
                          

    states_dict.remove((str(goal), right))



